Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		concat(leaf,Y)	→ Y
2:		concat(cons(U,V),Y)	→ cons(U,concat(V,Y))
3:		lessleaves(X,leaf)	→ false
4:		lessleaves(leaf,cons(W,Z))	→ true
5:		lessleaves(cons(U,V),cons(W,Z))	→ lessleaves(concat(U,V),concat(W,Z))

There are 4 dependency pairs:


6:		CONCAT(cons(U,V),Y)	→ CONCAT(V,Y)
7:		LESSLEAVES(cons(U,V),cons(W,Z))	→ LESSLEAVES(concat(U,V),concat(W,Z))
8:		LESSLEAVES(cons(U,V),cons(W,Z))	→ CONCAT(U,V)
9:		LESSLEAVES(cons(U,V),cons(W,Z))	→ CONCAT(W,Z)

The approximated dependency graph contains 2 SCCs: {6} and {7}.

Consider the SCC {6}. There are no usable rules. By taking the AF π with π(CONCAT) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 6 is strictly decreasing.

Consider the SCC {7}. The usable rules are {1,2}. The constraints could not be solved.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006